A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))  (ma-interface-ds(I;i)  x:Id fp Type) 

latex

Definitions	x:A. B(x), Id, fpf-domain(f), t  T, (x  l), b, IdDeq, P  Q, x. t(x), Type, a:A fp B(a), Knd, {x:A| B(x)} , State(ds), Top, left + right, x:AB(x), x:A  B(x), f(x), hasloc(k;i), x.A(x), t.1, ma-interface-ds(I;i), ma-interface-locs(I), MaInterface(T), P  Q, P & Q, P  Q
Lemmas	member-fpf-dom, pi1 wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, fpf-ap wf, id-deq wf, l member wf, fpf-domain wf